{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}

{- |
Copyright   : (c) Runtime Verification, 2022
License     : BSD-3-Clause

Attributes stored together with different entities in a
@KoreDefinition@.
-}
module Booster.Definition.Attributes.Base (
    DefinitionAttributes (..),
    defaultDefAttributes,
    ModuleAttributes (..),
    AxiomAttributes (..),
    Concreteness (..),
    Constrained (..),
    ComputedAxiomAttributes (..),
    SymbolType (..),
    FunctionType (..),
    SymbolAttributes (..),
    SMTType (..),
    SortAttributes (..),
    KCollectionTag (..),
    KCollectionSymbolNames (..),
    KCollectionMetadata (..),
    KMapDefinition (..),
    KListDefinition (..),
    KSetDefinition,
    Label,
    UniqueId (..),
    Location (..),
    Position (..),
    FileSource (..),
    Priority (..),
    pattern IsIdem,
    pattern IsNotIdem,
    pattern IsAssoc,
    pattern IsNotAssoc,
    pattern IsMacroOrAlias,
    pattern IsNotMacroOrAlias,
    pattern CanBeEvaluated,
    pattern CannotBeEvaluated,
    NotPreservesDefinednessReason (..),
) where

import Control.DeepSeq (NFData (..))
import Data.Aeson (ToJSON (..))
import Data.Aeson qualified as JSON
import Data.ByteString (ByteString)
import Data.Data (Data)
import Data.Hashable (Hashable)
import Data.Map (Map)
import Data.String
import Data.Text (Text)
import Data.Text.Encoding qualified as Text
import Data.Word (Word8)
import GHC.Generics (Generic)
import Language.Haskell.TH.Syntax (Lift)
import Prettyprinter as Pretty

import Booster.SMT.Base (SExpr)
import Booster.Util (Flag (..))
import Booster.Util qualified as Util

newtype DefinitionAttributes = DefinitionAttributes
    { indexCells :: [ByteString]
    -- ^ which cells to index for rewriting. Empty => default
    }
    deriving stock (Eq, Show, Generic)
    deriving anyclass (NFData)

defaultDefAttributes :: DefinitionAttributes
defaultDefAttributes = DefinitionAttributes []

data ModuleAttributes = ModuleAttributes
    {
    }
    -- none needed

    deriving stock (Eq, Show, Generic)
    deriving anyclass (NFData)

{- | Things needed for booster rewrite engine:
  * axiom location (for debug logging and error messages)
  * priority (to order and group axioms by descending priority)
  * label (to implement cut-point support)
-}
data AxiomAttributes = AxiomAttributes
    { location :: Maybe Location
    , priority :: Priority -- priorities are <= 200
    , ruleLabel :: Maybe Label
    , uniqueId :: UniqueId
    , simplification :: Flag "isSimplification"
    , preserving :: Flag "preservingDefinedness" -- this will override the computed attribute
    , concreteness :: Concreteness
    , smtLemma :: Flag "isSMTLemma"
    }
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

data ComputedAxiomAttributes = ComputedAxiomAttributes
    { containsAcSymbols :: Bool
    , notPreservesDefinednessReasons :: [NotPreservesDefinednessReason]
    }
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

newtype NotPreservesDefinednessReason = UndefinedSymbol ByteString
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

instance Pretty NotPreservesDefinednessReason where
    pretty = \case
        UndefinedSymbol name -> "non-total symbol " <> (pretty $ Text.decodeUtf8 $ Util.decodeLabel' name)

instance ToJSON NotPreservesDefinednessReason where
    toJSON (UndefinedSymbol n) = JSON.String $ Text.decodeUtf8 n

type Label = Text

newtype UniqueId = UniqueId {getUniqueId :: Text}
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

newtype Priority = Priority Word8
    deriving stock (Eq, Ord, Read, Show, Bounded)
    deriving newtype (Num, NFData)

newtype FileSource = FileSource FilePath
    deriving stock (Eq, Ord, Show)
    deriving newtype (IsString, NFData, Pretty)

data Location = Location
    { file :: FileSource
    , position :: Position
    }
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

instance Pretty Location where
    pretty Location{file, position} =
        Pretty.hsep [pretty file, ": ", pretty (position.line, position.column)]

data Position = Position
    { line :: Int
    , column :: Int
    }
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

data Constrained = Concrete | Symbolic
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

type VarnameAndSort = (ByteString, ByteString)

data Concreteness
    = Unconstrained
    | AllConstrained Constrained
    | SomeConstrained (Map VarnameAndSort Constrained)
    deriving stock (Eq, Ord, Show, Generic)
    deriving anyclass (NFData)

data FunctionType = Partial | Total
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data SymbolType
    = Function FunctionType
    | Constructor
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

pattern IsIdem, IsNotIdem :: Flag "isIdem"
pattern IsIdem = Flag True
pattern IsNotIdem = Flag False
{-# COMPLETE IsIdem, IsNotIdem #-}

pattern IsAssoc, IsNotAssoc :: Flag "isAssoc"
pattern IsAssoc = Flag True
pattern IsNotAssoc = Flag False
{-# COMPLETE IsAssoc, IsNotAssoc #-}

pattern IsMacroOrAlias, IsNotMacroOrAlias :: Flag "isMacroOrAlias"
pattern IsMacroOrAlias = Flag True
pattern IsNotMacroOrAlias = Flag False
{-# COMPLETE IsMacroOrAlias, IsNotMacroOrAlias #-}

pattern CanBeEvaluated, CannotBeEvaluated :: Flag "canBeEvaluated"
pattern CanBeEvaluated = Flag True
pattern CannotBeEvaluated = Flag False
{-# COMPLETE CanBeEvaluated, CannotBeEvaluated #-}

data SMTType
    = SMTLib ByteString
    | SMTHook SExpr
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data SymbolAttributes = SymbolAttributes
    { symbolType :: SymbolType
    , isIdem :: Flag "isIdem"
    , isAssoc :: Flag "isAssoc"
    , isMacroOrAlias :: Flag "isMacroOrAlias"
    , hasEvaluators :: Flag "canBeEvaluated"
    , collectionMetadata :: Maybe KCollectionMetadata
    , smt :: Maybe SMTType
    , hook :: Maybe ByteString
    }
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data KCollectionTag = KMapTag | KListTag | KSetTag
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data KCollectionMetadata
    = KMapMeta KMapDefinition
    | KListMeta KListDefinition
    | KSetMeta KSetDefinition
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data KCollectionSymbolNames = KCollectionSymbolNames
    { unitSymbolName :: ByteString
    , elementSymbolName :: ByteString
    , concatSymbolName :: ByteString
    }
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data KMapDefinition = KMapDefinition
    { symbolNames :: KCollectionSymbolNames
    , keySortName :: ByteString
    , elementSortName :: ByteString
    , mapSortName :: ByteString
    }
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

data KListDefinition = KListDefinition
    { symbolNames :: KCollectionSymbolNames
    , elementSortName :: ByteString
    , listSortName :: ByteString
    }
    deriving stock (Eq, Ord, Show, Generic, Data, Lift)
    deriving anyclass (NFData, Hashable)

type KSetDefinition = KListDefinition

data SortAttributes = SortAttributes
    { argCount :: Int
    , collectionAttributes :: Maybe (KCollectionSymbolNames, KCollectionTag)
    }
    deriving stock (Eq, Show, Generic)
    deriving anyclass (NFData)
